Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		even(0)	→ true
2:		even(s(0))	→ false
3:		even(s(s(x)))	→ even(x)
4:		half(0)	→ 0
5:		half(s(s(x)))	→ s(half(x))
6:		plus(0,y)	→ y
7:		plus(s(x),y)	→ s(plus(x,y))
8:		times(0,y)	→ 0
9:		times(s(x),y)	→ if_times(even(s(x)),s(x),y)
10:		if_times(true,s(x),y)	→ plus(times(half(s(x)),y),times(half(s(x)),y))
11:		if_times(false,s(x),y)	→ plus(y,times(x,y))

There are 10 dependency pairs:


12:		EVEN(s(s(x)))	→ EVEN(x)
13:		HALF(s(s(x)))	→ HALF(x)
14:		PLUS(s(x),y)	→ PLUS(x,y)
15:		TIMES(s(x),y)	→ IF_TIMES(even(s(x)),s(x),y)
16:		TIMES(s(x),y)	→ EVEN(s(x))
17:		IF_TIMES(true,s(x),y)	→ PLUS(times(half(s(x)),y),times(half(s(x)),y))
18:		IF_TIMES(true,s(x),y)	→ TIMES(half(s(x)),y)
19:		IF_TIMES(true,s(x),y)	→ HALF(s(x))
20:		IF_TIMES(false,s(x),y)	→ PLUS(y,times(x,y))
21:		IF_TIMES(false,s(x),y)	→ TIMES(x,y)

The approximated dependency graph contains 4 SCCs: {12}, {13}, {14} and {15,18,21}.

Consider the SCC {12}. There are no usable rules. By taking the AF π with π(EVEN) = 1 together with the lexicographic path order with empty precedence, rule 12 is strictly decreasing.

Consider the SCC {13}. There are no usable rules. By taking the AF π with π(HALF) = 1 together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.

Consider the SCC {14}. There are no usable rules. By taking the AF π with π(PLUS) = 1 together with the lexicographic path order with empty precedence, rule 14 is strictly decreasing.

Consider the SCC {15,18,21}. The usable rules are {1-5}. By taking the AF π with π(even) = π(half) = π(TIMES) = 1 and π(IF_TIMES) = 2 together with the lexicographic path order with precedence 0 ≻ false and 0 ≻ true, the rules in {4,15,18} are weakly decreasing and the rules in {1-3,5,21} are strictly decreasing. There is one new SCC.
- Consider the SCC {15,18}. The constraints could not be solved.

Tyrolean Termination Tool (0.26 seconds) --- May 4, 2006